$\forall$${\it the\_es}$:ES, $e$, ${\it e'}$:E.
\\[0ex]($e$ $<$ ${\it e'}$)
\\[0ex]$\Leftrightarrow$
\\[0ex]$\neg$first(${\it e'}$) \& ($e$ $<$ pred(${\it e'}$)) $\vee$ $e$ $=$ pred(${\it e'}$) $\vee$ isrcv(${\it e'}$) \& ($e$ $<$ sender(${\it e'}$)) $\vee$ $e$ $=$ sender(${\it e'}$)